1. Field of Invention
The present invention relates to a method and apparatus for reducing the complexity of a representation of a hardware system.
2. Description of the Prior Art
The first stage in synthesizing and proving the properties of a system is a compilation process in which the system is modeled by representation as a set of functions comprising a first subset of functions which determines the value of system outputs as a function of system inputs, system states represented by state bits, and internal signals; a second subset of functions which determines the values of state bits on the next clock cycle as a function of system inputs, system states represented by state bits, and internal signals; and a third subset of functions which determines the values of internal signals as a function of system inputs, system states, and internal signals.
To enable or accelerate formal proof of the system and its properties, internal signals may be eliminated from the system model by substituting them into the functions which refer to them. In the course of this substitution, the representation of the model may become extremely large. If this occurs, it is possible to detect an explosion in the size of the representation and to suspend the substitution process while restructuring the representation to seek a reduction in size.
Typically in a compilation process, static relationships between signals in the system model can be destroyed by dynamic restructuring operations. This can lead to a further explosion later during the substitution process.
It would be advantageous to take static relationships into account during the dynamic restructuring process.
One technique of representing functions and internal signals is by the use of binary decision diagrams (BDD's). A binary decision diagram is a representation of a digital function which contains the information necessary to implement the function. The diagram is a tree-like structure having a root and plural nodes, where the root represents the digital function and the nodes are labeled with variables. Each node has two branches, one representing the assertion that the variable labeling the node is 1, and the other representing the assertion that the variable labeling the node is 0. In a BDD, “ordering” relates to the order in which variable names are encountered during traversal of the graph. Better orderings result in fewer nodes in the graph.